COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002								    NIC 24934
C00011 ENDMK
C⊗;
							    NIC 24934
						    Part of NIC 24980

	STANFORD ARTIFICIAL INTELLIGENCE LABORATORY
  		1974 ARPA Project Summary
Prepared for:	ARPA IPTO Principal Investigators Meeting
		March 12-14, 1975

Prepared by:	John McCarthy
		Computer Science Department
		Stanford University
		Stanford, California 94305

Formal Reasoning -- John McCarthy, Richard Weyhrauch, et al

Using our  LCF proof-checker, we  have produced an  axiomatization of
the programming language PASCAL.  This represents a major step toward
using LCF as a practical program verification system. 

Newey in his thesis used LCF to prove the partial correctness of the
LISP 1.5 interpreter and began a project to prove the correctness
of a LISP compiler (called LCOM0).  This compiler is actually more than
a toy in that it is used in the LISP course here at Stanford.  This
thesis as a whole represented a kind of case study which demonstrated
our ability to check the correctness large LISP programs.

Automatic Deduction -- David Luckham, et al

A successful new automatic programming system accepts descriptions of
library routines,  programming methods, and program specifications in
a high  level  semantic definition  language.   It  returns  programs
written  in a subset of  ALGOL that satisfy the given specifications. 
Experimental  applications  include computing  arithmetical functions
and planning robot strategies. 

Another system  works  with algorithms  expressed  in a  higher-level
language  and automatically chooses  an efficient  representation for
the data  structure.   It  then produces  a  program that  uses  this
representation.  Representations considered include  certain kinds of
linked-lists, binary trees, and hash tables. 

Program Understanding Systems -- Cordell Green, et al

The EXAMPLE program  that infers recursive  list-processing functions
from  example input-output  pairs was  completed  during 1974.   This
system demonstrates the possibility  of using fairly natural  methods
of program specification. 

The  PUP  system  was  our  first  to  show  a  rudimentary  "program
understanding"  behavior.  By following a  simple chain of reasoning,
it can  synthesize  a  few short  programs,  such as  interchange  of
elements, three-element sort, and integer square root. 

A system was  completed which, given a program  expressed in terms of
high-level information  structures such  as sets,  ordered sets,  and
relations,  automatically   chooses  efficient   implementation-level
representations  and produces an  equivalent program  that uses these
representations. 

A very comprehensive dialog was completed which exhibits  a knowledge
base of  rules for the  synthesis of sorting programs.   Although not
all  the   necessary  synthesis  rules  have  been  codified,  it  is
reasonably clear how  to do so.   This work  is aimed at the  deepest
understanding of a simple program synthesis yet attempted. 

Work was  completed on a pilot system  that interactively synthesizes
what is essentially Winston's concept formation program.  This system
points  toward   the  feasibility  of   systems  for   writing  long,
domain-specific programs. 

Natural Language Understanding -- Terry Winograd, et al

A system was completed that links natural language
understanding, inference, and generation of natural language output.
This is the first such system with a strong theoretical basis, namely
Conceptual Dependency.

Work was begun on a knowledge representation language for natural
language systems which combines the advantages of procedural and
declarative formalisms.  It will be developed over the next three
years as the basis for several understander projects.

Hand-eye Research -- Tom Binford, Lynn Quam, et al

We have used near and far field stereo  vision and motion parallax to
locate  objects spatially and to automatically generate contour maps. 

We completed design of a manipulation system AL, which combines
a control language with a planning system to aid in extended tasks
such as assembly.  AL has new features  such as:
ALGOL-like control; interrupts and control monitors; simultaneous
coordinted motion of two or more arms; 
and a planning system.  The implementation is well
underway.  The planning system includes a subsystem for
keeping track of the locus of parts, translating semantic constraints
into mathematical constraints.

We completed assembly of a hinge
using two arms in coordinated non-simultaneous motion.
We have carried out two subassemblies of a two stroke gasoline engine.

We have completed some modules of a visual system
to be used for control of assembly.  The system has facilities for
manual generation of 2D symbolic models, matching of curves
in an image with those of the model.  The system has the
facility for using 3D models, as in CAD, predicting symbolic 2D
models from 3D.

We have also completed recognition of complex objects
such as a doll and a toy horse
using the spine-cross section representation.
The system forms its own models, and matches in a way suitable for a large
visual memory, by making summary descriptions which it uses to find
a subclass of models similar to the test object.

Training

During the last year, eleven members   of  our  staff   published  Ph.D.
dissertations  and  another  32  graduate  students  received  direct
support.